le2(0, y) -> true
le2(s1(x), 0) -> false
le2(s1(x), s1(y)) -> le2(x, y)
minus2(x, 0) -> x
minus2(s1(x), s1(y)) -> minus2(x, y)
mod2(0, y) -> 0
mod2(s1(x), 0) -> 0
mod2(s1(x), s1(y)) -> if_mod3(le2(y, x), s1(x), s1(y))
if_mod3(true, s1(x), s1(y)) -> mod2(minus2(x, y), s1(y))
if_mod3(false, s1(x), s1(y)) -> s1(x)
↳ QTRS
↳ Non-Overlap Check
le2(0, y) -> true
le2(s1(x), 0) -> false
le2(s1(x), s1(y)) -> le2(x, y)
minus2(x, 0) -> x
minus2(s1(x), s1(y)) -> minus2(x, y)
mod2(0, y) -> 0
mod2(s1(x), 0) -> 0
mod2(s1(x), s1(y)) -> if_mod3(le2(y, x), s1(x), s1(y))
if_mod3(true, s1(x), s1(y)) -> mod2(minus2(x, y), s1(y))
if_mod3(false, s1(x), s1(y)) -> s1(x)
↳ QTRS
↳ Non-Overlap Check
↳ QTRS
↳ DependencyPairsProof
le2(0, y) -> true
le2(s1(x), 0) -> false
le2(s1(x), s1(y)) -> le2(x, y)
minus2(x, 0) -> x
minus2(s1(x), s1(y)) -> minus2(x, y)
mod2(0, y) -> 0
mod2(s1(x), 0) -> 0
mod2(s1(x), s1(y)) -> if_mod3(le2(y, x), s1(x), s1(y))
if_mod3(true, s1(x), s1(y)) -> mod2(minus2(x, y), s1(y))
if_mod3(false, s1(x), s1(y)) -> s1(x)
le2(0, x0)
le2(s1(x0), 0)
le2(s1(x0), s1(x1))
minus2(x0, 0)
minus2(s1(x0), s1(x1))
mod2(0, x0)
mod2(s1(x0), 0)
mod2(s1(x0), s1(x1))
if_mod3(true, s1(x0), s1(x1))
if_mod3(false, s1(x0), s1(x1))
LE2(s1(x), s1(y)) -> LE2(x, y)
IF_MOD3(true, s1(x), s1(y)) -> MINUS2(x, y)
MINUS2(s1(x), s1(y)) -> MINUS2(x, y)
MOD2(s1(x), s1(y)) -> IF_MOD3(le2(y, x), s1(x), s1(y))
IF_MOD3(true, s1(x), s1(y)) -> MOD2(minus2(x, y), s1(y))
MOD2(s1(x), s1(y)) -> LE2(y, x)
le2(0, y) -> true
le2(s1(x), 0) -> false
le2(s1(x), s1(y)) -> le2(x, y)
minus2(x, 0) -> x
minus2(s1(x), s1(y)) -> minus2(x, y)
mod2(0, y) -> 0
mod2(s1(x), 0) -> 0
mod2(s1(x), s1(y)) -> if_mod3(le2(y, x), s1(x), s1(y))
if_mod3(true, s1(x), s1(y)) -> mod2(minus2(x, y), s1(y))
if_mod3(false, s1(x), s1(y)) -> s1(x)
le2(0, x0)
le2(s1(x0), 0)
le2(s1(x0), s1(x1))
minus2(x0, 0)
minus2(s1(x0), s1(x1))
mod2(0, x0)
mod2(s1(x0), 0)
mod2(s1(x0), s1(x1))
if_mod3(true, s1(x0), s1(x1))
if_mod3(false, s1(x0), s1(x1))
↳ QTRS
↳ Non-Overlap Check
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
LE2(s1(x), s1(y)) -> LE2(x, y)
IF_MOD3(true, s1(x), s1(y)) -> MINUS2(x, y)
MINUS2(s1(x), s1(y)) -> MINUS2(x, y)
MOD2(s1(x), s1(y)) -> IF_MOD3(le2(y, x), s1(x), s1(y))
IF_MOD3(true, s1(x), s1(y)) -> MOD2(minus2(x, y), s1(y))
MOD2(s1(x), s1(y)) -> LE2(y, x)
le2(0, y) -> true
le2(s1(x), 0) -> false
le2(s1(x), s1(y)) -> le2(x, y)
minus2(x, 0) -> x
minus2(s1(x), s1(y)) -> minus2(x, y)
mod2(0, y) -> 0
mod2(s1(x), 0) -> 0
mod2(s1(x), s1(y)) -> if_mod3(le2(y, x), s1(x), s1(y))
if_mod3(true, s1(x), s1(y)) -> mod2(minus2(x, y), s1(y))
if_mod3(false, s1(x), s1(y)) -> s1(x)
le2(0, x0)
le2(s1(x0), 0)
le2(s1(x0), s1(x1))
minus2(x0, 0)
minus2(s1(x0), s1(x1))
mod2(0, x0)
mod2(s1(x0), 0)
mod2(s1(x0), s1(x1))
if_mod3(true, s1(x0), s1(x1))
if_mod3(false, s1(x0), s1(x1))
↳ QTRS
↳ Non-Overlap Check
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
↳ AND
↳ QDP
↳ QDPOrderProof
↳ QDP
↳ QDP
MINUS2(s1(x), s1(y)) -> MINUS2(x, y)
le2(0, y) -> true
le2(s1(x), 0) -> false
le2(s1(x), s1(y)) -> le2(x, y)
minus2(x, 0) -> x
minus2(s1(x), s1(y)) -> minus2(x, y)
mod2(0, y) -> 0
mod2(s1(x), 0) -> 0
mod2(s1(x), s1(y)) -> if_mod3(le2(y, x), s1(x), s1(y))
if_mod3(true, s1(x), s1(y)) -> mod2(minus2(x, y), s1(y))
if_mod3(false, s1(x), s1(y)) -> s1(x)
le2(0, x0)
le2(s1(x0), 0)
le2(s1(x0), s1(x1))
minus2(x0, 0)
minus2(s1(x0), s1(x1))
mod2(0, x0)
mod2(s1(x0), 0)
mod2(s1(x0), s1(x1))
if_mod3(true, s1(x0), s1(x1))
if_mod3(false, s1(x0), s1(x1))
The following pairs can be strictly oriented and are deleted.
The remaining pairs can at least by weakly be oriented.
MINUS2(s1(x), s1(y)) -> MINUS2(x, y)
trivial
↳ QTRS
↳ Non-Overlap Check
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
↳ AND
↳ QDP
↳ QDPOrderProof
↳ QDP
↳ PisEmptyProof
↳ QDP
↳ QDP
le2(0, y) -> true
le2(s1(x), 0) -> false
le2(s1(x), s1(y)) -> le2(x, y)
minus2(x, 0) -> x
minus2(s1(x), s1(y)) -> minus2(x, y)
mod2(0, y) -> 0
mod2(s1(x), 0) -> 0
mod2(s1(x), s1(y)) -> if_mod3(le2(y, x), s1(x), s1(y))
if_mod3(true, s1(x), s1(y)) -> mod2(minus2(x, y), s1(y))
if_mod3(false, s1(x), s1(y)) -> s1(x)
le2(0, x0)
le2(s1(x0), 0)
le2(s1(x0), s1(x1))
minus2(x0, 0)
minus2(s1(x0), s1(x1))
mod2(0, x0)
mod2(s1(x0), 0)
mod2(s1(x0), s1(x1))
if_mod3(true, s1(x0), s1(x1))
if_mod3(false, s1(x0), s1(x1))
↳ QTRS
↳ Non-Overlap Check
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
↳ AND
↳ QDP
↳ QDP
↳ QDPOrderProof
↳ QDP
LE2(s1(x), s1(y)) -> LE2(x, y)
le2(0, y) -> true
le2(s1(x), 0) -> false
le2(s1(x), s1(y)) -> le2(x, y)
minus2(x, 0) -> x
minus2(s1(x), s1(y)) -> minus2(x, y)
mod2(0, y) -> 0
mod2(s1(x), 0) -> 0
mod2(s1(x), s1(y)) -> if_mod3(le2(y, x), s1(x), s1(y))
if_mod3(true, s1(x), s1(y)) -> mod2(minus2(x, y), s1(y))
if_mod3(false, s1(x), s1(y)) -> s1(x)
le2(0, x0)
le2(s1(x0), 0)
le2(s1(x0), s1(x1))
minus2(x0, 0)
minus2(s1(x0), s1(x1))
mod2(0, x0)
mod2(s1(x0), 0)
mod2(s1(x0), s1(x1))
if_mod3(true, s1(x0), s1(x1))
if_mod3(false, s1(x0), s1(x1))
The following pairs can be strictly oriented and are deleted.
The remaining pairs can at least by weakly be oriented.
LE2(s1(x), s1(y)) -> LE2(x, y)
trivial
↳ QTRS
↳ Non-Overlap Check
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
↳ AND
↳ QDP
↳ QDP
↳ QDPOrderProof
↳ QDP
↳ PisEmptyProof
↳ QDP
le2(0, y) -> true
le2(s1(x), 0) -> false
le2(s1(x), s1(y)) -> le2(x, y)
minus2(x, 0) -> x
minus2(s1(x), s1(y)) -> minus2(x, y)
mod2(0, y) -> 0
mod2(s1(x), 0) -> 0
mod2(s1(x), s1(y)) -> if_mod3(le2(y, x), s1(x), s1(y))
if_mod3(true, s1(x), s1(y)) -> mod2(minus2(x, y), s1(y))
if_mod3(false, s1(x), s1(y)) -> s1(x)
le2(0, x0)
le2(s1(x0), 0)
le2(s1(x0), s1(x1))
minus2(x0, 0)
minus2(s1(x0), s1(x1))
mod2(0, x0)
mod2(s1(x0), 0)
mod2(s1(x0), s1(x1))
if_mod3(true, s1(x0), s1(x1))
if_mod3(false, s1(x0), s1(x1))
↳ QTRS
↳ Non-Overlap Check
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
↳ AND
↳ QDP
↳ QDP
↳ QDP
↳ QDPOrderProof
MOD2(s1(x), s1(y)) -> IF_MOD3(le2(y, x), s1(x), s1(y))
IF_MOD3(true, s1(x), s1(y)) -> MOD2(minus2(x, y), s1(y))
le2(0, y) -> true
le2(s1(x), 0) -> false
le2(s1(x), s1(y)) -> le2(x, y)
minus2(x, 0) -> x
minus2(s1(x), s1(y)) -> minus2(x, y)
mod2(0, y) -> 0
mod2(s1(x), 0) -> 0
mod2(s1(x), s1(y)) -> if_mod3(le2(y, x), s1(x), s1(y))
if_mod3(true, s1(x), s1(y)) -> mod2(minus2(x, y), s1(y))
if_mod3(false, s1(x), s1(y)) -> s1(x)
le2(0, x0)
le2(s1(x0), 0)
le2(s1(x0), s1(x1))
minus2(x0, 0)
minus2(s1(x0), s1(x1))
mod2(0, x0)
mod2(s1(x0), 0)
mod2(s1(x0), s1(x1))
if_mod3(true, s1(x0), s1(x1))
if_mod3(false, s1(x0), s1(x1))
The following pairs can be strictly oriented and are deleted.
The remaining pairs can at least by weakly be oriented.
MOD2(s1(x), s1(y)) -> IF_MOD3(le2(y, x), s1(x), s1(y))
IF_MOD3(true, s1(x), s1(y)) -> MOD2(minus2(x, y), s1(y))
s1 > le > true > MOD1 > IFMOD1
s1 > le > false > IFMOD1
0 > true > MOD1 > IFMOD1
0 > false > IFMOD1
le2(0, y) -> true
le2(s1(x), 0) -> false
le2(s1(x), s1(y)) -> le2(x, y)
minus2(x, 0) -> x
minus2(s1(x), s1(y)) -> minus2(x, y)
↳ QTRS
↳ Non-Overlap Check
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
↳ AND
↳ QDP
↳ QDP
↳ QDP
↳ QDPOrderProof
↳ QDP
↳ PisEmptyProof
le2(0, y) -> true
le2(s1(x), 0) -> false
le2(s1(x), s1(y)) -> le2(x, y)
minus2(x, 0) -> x
minus2(s1(x), s1(y)) -> minus2(x, y)
mod2(0, y) -> 0
mod2(s1(x), 0) -> 0
mod2(s1(x), s1(y)) -> if_mod3(le2(y, x), s1(x), s1(y))
if_mod3(true, s1(x), s1(y)) -> mod2(minus2(x, y), s1(y))
if_mod3(false, s1(x), s1(y)) -> s1(x)
le2(0, x0)
le2(s1(x0), 0)
le2(s1(x0), s1(x1))
minus2(x0, 0)
minus2(s1(x0), s1(x1))
mod2(0, x0)
mod2(s1(x0), 0)
mod2(s1(x0), s1(x1))
if_mod3(true, s1(x0), s1(x1))
if_mod3(false, s1(x0), s1(x1))